$\forall$$A$, $B$:Type, $x$:$A$, $y$:$B$. ((inr $y$ ) = (inl $x$ ) $\in$ ($A$ + $B$)) $\Rightarrow$ False